COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.at "Goedel" ⊂"G%B:%*odel"⊃
.font B "Zero30"

	Several people have commented that the minimization schema
seems to be creeping second order logic.  Indeed it steps beyond the
axiom schema of induction of Peano arithmetic in that we have
a schema for each function rather than a single schema.  However,
our method of proof using it as implemented in Richard Weyhrauch's
proof-checker and interactive theorem prover FOL is still basically
first order.  It has the weakness of all first order systems in
that it doesn't permit proving statements that quantify over functions.
It has the strength that the Goedelian incompleteness is in the
axiomatization rather than in the logic.  Moreover, R. S. Cartwright
has recently shown that any sentence containing a function characterized
by a functional equation and minimization schema can be proved in
first order logic to be equivalent to a sentence not involving the
function but only ⊗car, ⊗cdr, ⊗cons, ⊗atom and ⊗occur.  Thus the
incompleteness is in the axiomatization of the domain rather than
in the logic.  I think this is the essence of the issue as to whether
the logic is first or second order.

	Although we don't have much practical experience with the
minimization schema, we have used it to prove partial
correctness and to prove that a function is not total.  Mostly
the comparison functions have not been recursive, but it has
also been used to get results formerly proved with my now retired
method of recursion induction.  On the whole, it looks convenient.